Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		dbl(0)	→ 0
2:		dbl(s(X))	→ s(s(dbl(X)))
3:		dbls(nil)	→ nil
4:		dbls(cons(X,Y))	→ cons(dbl(X),dbls(Y))
5:		sel(0,cons(X,Y))	→ X
6:		sel(s(X),cons(Y,Z))	→ sel(X,Z)
7:		indx(nil,X)	→ nil
8:		indx(cons(X,Y),Z)	→ cons(sel(X,Z),indx(Y,Z))
9:		from(X)	→ cons(X,from(s(X)))

There are 7 dependency pairs:


10:		DBL(s(X))	→ DBL(X)
11:		DBLS(cons(X,Y))	→ DBL(X)
12:		DBLS(cons(X,Y))	→ DBLS(Y)
13:		SEL(s(X),cons(Y,Z))	→ SEL(X,Z)
14:		INDX(cons(X,Y),Z)	→ SEL(X,Z)
15:		INDX(cons(X,Y),Z)	→ INDX(Y,Z)
16:		FROM(X)	→ FROM(s(X))

The approximated dependency graph contains 5 SCCs: {10}, {12}, {16}, {13} and {15}.

Consider the SCC {10}. There are no usable rules. By taking the AF π with π(DBL) = 1 together with the lexicographic path order with empty precedence, rule 10 is strictly decreasing.

Consider the SCC {12}. There are no usable rules. By taking the AF π with π(DBLS) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {16}. There are no usable rules. The constraints could not be solved.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(SEL) = 1 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {15}. There are no usable rules. By taking the AF π with π(INDX) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 15 is strictly decreasing.

Tyrolean Termination Tool (0.02 seconds) --- May 3, 2006